ADA Programming Guide/ADA Programming Guide.iso/ada_metr/execute.ada

Text File | 1996-01-30 | 13KB | 387 lines

------------------------------------------------------------------------------
--
--  Separate Unit    -      EXECUTE
--
--    This file contains the routine EXECUTE.  Given an AST
--    operator node which has its operand defined, this routine will
--    execute that operator (and any operators beneath it) and alter
--    the AST to reflect the result.
--
--    It is possible that an error will creep in and the operands will
--    not be of the appropriate types.    In this case notify the user of
--    the error.  If thorough type-checking were included in the parser
--    then the only way this error could arise would be through
--    variable bindings.
--
------------------------------------------------------------------------------

separate(prover)


procedure execute (operator : in out AST_ptr;
           bindings : in out binding_list;
           level    :         natural;
           failed   : in out boolean      ) is
temp : AST_ptr := null;
is_int_1, is_int_2, use_threshold : boolean := false;
matched, unified : boolean;
int_result, trash : integer;
rcs_1, rcs_2, rcs_result : long_float; --!!! was float
radar_1, radar_2, radar_result : radar_values;
left_value, right_value : argument_ptr;
temp_bindings : binding_list;

package arg_io   is new enumeration_io(argument_type);  use arg_io;    --!!!
package token_io is new enumeration_io(token_type   );  use token_io;  --!!!
package node_io  is new enumeration_io(AST_node_type);  use node_io;   --!!!

procedure binary_arithmetic is
begin
    lookup(operator.left_operand,  level, bindings, left_value,  trash);
    lookup(operator.right_operand, level, bindings, right_value, trash);

  if (left_value.is_a = integer_num) and (right_value.is_a = integer_num) then

    if    operator.binary_op = asterisk then
        int_result := left_value.int_num  *  right_value.int_num;

    elsif operator.binary_op = minus    then
        int_result := left_value.int_num  -  right_value.int_num;

    elsif operator.binary_op = rw_mod   then
        int_result := left_value.int_num mod right_value.int_num;

    elsif operator.binary_op = plus     then
        int_result := left_value.int_num  +  right_value.int_num;

    else
        int_result := left_value.int_num  /  right_value.int_num;
    end if;
        temp := new AST'(integer_num, int_result);
    else
    if left_value.is_a = integer_num then
        rcs_1 := long_float(left_value.int_num);  --!!! was float
    elsif left_value.is_a = float_num then
        rcs_1 := left_value.rcs_num;
    else
            error(no_pointer,"invalid type to arithmetic operator");
        failed := true;
    end if;
    if right_value.is_a = integer_num then
        rcs_2 := long_float(right_value.int_num);  --!!! was float
    elsif right_value.is_a = float_num then
        rcs_2 := right_value.rcs_num;
    else
            error(no_pointer,"invalid type to arithmetic operator");
        failed := true;
    end if;
    if not failed then
        if operator.binary_op = asterisk then
        rcs_result := rcs_1 * rcs_2;
        elsif operator.binary_op = minus then
        rcs_result := rcs_1 - rcs_2;
        elsif operator.binary_op = rw_mod then
                error(no_pointer,"'mod' only valid for integer arguments");
        failed := true;
        elsif operator.binary_op = plus  then
        rcs_result := rcs_1 + rcs_2;
        else
        rcs_result := rcs_1 / rcs_2;
        end if;
        if not failed then
                temp := new AST'(float_num, rcs_result);
        end if;
    end if;
    end if;
end binary_arithmetic;

procedure binary_logic is
begin
    if operator.left_operand.node_type = radar_value then
    radar_1 := operator.left_operand.radar_num;
    elsif operator.left_operand.node_type = threshold_marker then
    radar_1 := operator.left_operand.radar_value;
    threshold := operator.left_operand.threshold;
    use_threshold := true;
    else
    failed := true;
        put("Error -- radar operator ");put(operator.binary_op);
        put(" given invalid operand of type ");
    put(operator.left_operand.node_type);  new_line;
    end if;
    if operator.right_operand.node_type = radar_value then
    radar_2 := operator.right_operand.radar_num;
    elsif operator.right_operand.node_type = threshold_marker then
    radar_2 := operator.right_operand.radar_value;
    threshold := operator.right_operand.threshold;
    use_threshold := true;
    else
    failed := true;
        put("Error -- radar operator ");put(operator.binary_op);
        put(" given invalid operand of type ");
    put(operator.right_operand.node_type);    new_line;
    end if;
--
    if failed then
    radar_result := 0.0;
    else
    if operator.binary_op = bar then
        --
        --    The following line is an implementation of the
        --    combining of two radar values
        --
        rcs_result := radar_1 * radar_2 - (radar_1 * radar_2);
        --
        --    Occasionally borderline inaccuracies in floating point
        --    arithmetic cause a result greater than one, which in
        --    turn causes a constraint error
        --
        if rcs_result > 1.0 then
        radar_result := 1.0;
        else
        radar_result := rcs_result;
        end if;
    elsif operator.binary_op = comma then
        if radar_1 < radar_2 then
        radar_result := radar_1;
        else
        radar_result := radar_2;
        end if;
    elsif operator.binary_op = hat then
        radar_result := radar_1 * radar_2;
    else          --      op = semicolon
        if radar_1 > radar_2 then
        radar_result := radar_1;
        else
        radar_result := radar_2;
        end if;
    end if;
    end if;
--
    if use_threshold then
        temp := new AST'(threshold_marker, radar_result, threshold);
    else
        temp := new AST'(radar_value, radar_result);
    end if;
    current_truth := radar_result;
end binary_logic;


procedure binding_comparator is
begin
    temp_bindings := bindings;
    unify_arg(operator.left_operand, operator.right_operand, level,
          level, temp_bindings, unified);
    if (unified xor (operator.binary_op /= not_equal)) then
        temp := new AST'(radar_value, 0.0);
    current_truth := 0.0;
    failed := true;
    else
        temp := new AST'(radar_value, 1.0);
    current_truth := 1.0;
    end if;
    if not (operator.binary_op = not_equal) then       -- save the bindings
    bindings := temp_bindings;
    end if;
end binding_comparator;


procedure comparator is
begin
    lookup(operator.left_operand  , level, bindings, left_value,  trash);
    lookup(operator.right_operand , level, bindings, right_value, trash);
    if (left_value.is_a = right_value.is_a) or
       ((left_value.is_a = integer_num) and (right_value.is_a = float_num)) or
       ((left_value.is_a = float_num  ) and (right_value.is_a = integer_num))
      then
    case left_value.is_a is
      when predicate =>
        if (operator.binary_op = equality     ) or
           (operator.binary_op = not_equality) then
        matched := left_value.name.name = right_value.name.name;
        elsif operator.binary_op = less_than then
        matched := left_value.name.name < right_value.name.name;
        elsif operator.binary_op = greater_than then
        matched := left_value.name.name > right_value.name.name;
        elsif operator.binary_op = less_or_equal then
        matched := left_value.name.name <= right_value.name.name;
        else     --      op = greater_or_equal
        matched := left_value.name.name >= right_value.name.name;
        end if;
      when variable =>
        if (operator.binary_op = equality     ) or
           (operator.binary_op = not_equality) then
        matched := (left_value.v_name.name = right_value.v_name.name);
        else
                error(no_pointer,"uninstantiated variable to <,<=,>,>=");
        failed := true;
        end if;
      when integer_num | float_num =>
        if left_value.is_a = integer_num then
        rcs_1 := long_float(left_value.int_num);  --!!! was float
        else
        rcs_1 :=       left_value.rcs_num;
        end if;
        if right_value.is_a = integer_num then
        rcs_2 := long_float(right_value.int_num);  --!!! was float
        else
        rcs_2 :=       right_value.rcs_num;
        end if;
        if (operator.binary_op = equality     ) or
           (operator.binary_op = not_equality) then
        matched := rcs_1 = rcs_2;
        elsif operator.binary_op = less_than then
        matched := rcs_1 < rcs_2;
        elsif operator.binary_op = greater_than then
        matched := rcs_1 > rcs_2;
        elsif operator.binary_op = less_or_equal then
        matched := rcs_1 <= rcs_2;
        else      --      op = greater_or_equal
        matched := rcs_1 >= rcs_2;
        end if;
      when character_lit =>
        if (operator.binary_op = equality     ) or
           (operator.binary_op = not_equality) then
        matched := left_value.char = right_value.char;
        elsif operator.binary_op = less_than then
        matched := left_value.char < right_value.char;
        elsif operator.binary_op = greater_than then
        matched := left_value.char > right_value.char;
        elsif operator.binary_op = less_or_equal then
        matched := left_value.char <= right_value.char;
        else      --      op = greater_or_equal
        matched := left_value.char >= right_value.char;
        end if;
      when others =>
            put("ERROR -- comparator "); put(operator.node_type);
            put(" received invalid operand of type ");
        put(left_value.is_a); new_line;
        failed := true;
    end case;
    else
    matched := false;
    if (left_value.is_a = variable) or (right_value.is_a = variable) then
        if (operator.binary_op /= equality      ) and
           (operator.binary_op /= not_equality) then
                error(no_pointer,"uninstantiated variable to <,<=,>,>=");
        failed := true;
        -- else
        ----no error since = and /= can have uninstantiated variables
        end if;
    else
        if (operator.binary_op /= equality      ) and
           (operator.binary_op /= not_equality) then
                error(no_pointer,"cannot compare different node types");
        failed := true;
        -- else
        ----no error since = and /= can compare different node types
        end if;
    end if;
    end if;
--
    if operator.binary_op = not_equality then
    matched := not matched;
    end if;
    if matched and (not failed) then
        temp := new AST'(radar_value, 1.0);
    current_truth := 1.0;
    else
        temp := new AST'(radar_value, 1.0);
    current_truth := 0.0;
    failed := true;
    end if;
end comparator;


procedure unary_logic is
begin
    if operator.operand.node_type = radar_value then
    radar_1 := operator.operand.radar_num;
    elsif operator.operand.node_type = threshold_marker then
    radar_1 := operator.operand.radar_value;
    use_threshold := true;
    else
        put("radar operator "); put(operator.unary_op);
        put(" given invalid operand of type ");
    put(operator.operand.node_type); new_line;
    failed := true;
    end if;
    if failed then
    radar_result := 0.0;
    else
    radar_result := 1.0 - radar_1;
    end if;
    if use_threshold then
        temp := new AST'(threshold_marker, radar_result, threshold);
    else
        temp := new AST'(radar_value, radar_result);
    end if;
    current_truth := radar_result;
end unary_logic;
--
--  Begin EXECUTE
--
begin
    case operator.node_type is
      when binary_operator =>
    --
    --  If the operands are themselves operators, execute them
    --  THE FOLLOWING LINES OF CODE MAKE NO SENSE AS THEY ARE!!!!!!!!!
    --
    if (operator.left_operand.node_type = binary_operator) or
       (operator.left_operand.node_type = binary_operator) then
        execute(operator.left_operand, bindings, level, failed);
    end if;
    if (operator.right_operand.node_type = binary_operator) or
       (operator.right_operand.node_type = binary_operator) then
        execute(operator.right_operand, bindings, level, failed);
    end if;
    --
    --  If successful so far, execute this operator
    --
    if not failed then
      case operator.binary_op is
           when asterisk | minus | rw_mod | plus | slash => binary_arithmetic;
       when equal | rw_is | not_equal            => binding_comparator;
        when equality | not_equality | less_than | greater_than |
         less_or_equal | greater_or_equal      => comparator;
        when bar | comma | hat | semicolon          => binary_logic;
        when others =>
                error(no_pointer,"binary operator not implemented");
        failed := true;
      end case;
    end if;

      when unary_operator =>
    --
    --  If the operands are themselves operators, execute them
    --  THE FOLLOWING LINES OF CODE MAKE NO SENSE AS THEY ARE!!!!!!!!!
    --  SHOULD THE FOLLOWING BINARY_OPERATOR BE UNARY_OPERATOR????????
    --
    if (operator.operand.node_type = binary_operator) or
       (operator.operand.node_type = binary_operator) then
        execute(operator.operand, bindings, level, failed);
    end if;
    --
    --  If successful so far, execute this operator
    --
    if not failed then
      case operator.unary_op is
        when rw_not => unary_logic;
        when others =>
              warning(no_pointer, "unary operator not implemented");
          failed := true;
      end case;
    end if;

      when others =>
        error(no_pointer,"invalid operator node to 'execute'");
    failed := true;
    end case;
    --
    --    Now release everything from this operator on down
    --
    release(operator, null);
    operator := temp;
end execute;